;;; -*- Mode: Lisp; Syntax: Common-Lisp; Package: snark -*-
;;; File: tree-index.lisp
;;; The contents of this file are subject to the Mozilla Public License
;;; Version 1.1 (the "License"); you may not use this file except in
;;; compliance with the License. You may obtain a copy of the License at
;;; http://www.mozilla.org/MPL/
;;;
;;; Software distributed under the License is distributed on an "AS IS"
;;; basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See the
;;; License for the specific language governing rights and limitations
;;; under the License.
;;;
;;; The Original Code is SNARK.
;;; The Initial Developer of the Original Code is SRI International.
;;; Portions created by the Initial Developer are Copyright (C) 1981-2006.
;;; All Rights Reserved.
;;;
;;; Contributor(s): Mark E. Stickel <stickel@ai.sri.com>.

(in-package :snark)

(defvar *tree-index*)

(defstruct (tree-index
	     (:constructor make-tree-index0 (entry-constructor))
	     (:copier nil))
  (entry-constructor nil :read-only t)		;term->entry function for new entry insertion
  (node-counter (make-counter 1) :read-only t)
  (entry-counter (make-counter) :read-only t)
  (top-node (make-tree-index-internal-node) :read-only t))

(defstruct (tree-index-node
	     (:copier nil))
  (parent-node nil :read-only t))

(defstruct (tree-index-internal-node
            (:include tree-index-node)
            (:copier nil))
  (variable-child-node nil)			;nil or node
  (constant-indexed-child-nodes nil)		;constant# -> node sparse-vector
  (function-indexed-child-nodes nil))		;function# -> node sparse-vector

(defstruct (tree-index-leaf-node
	     (:include tree-index-node)
	     (:copier nil))
  (entries (make-sparse-vector :default-value none) :read-only t)
  (mark nil))

(defstruct (index-entry
	     (:constructor make-index-entry (term))
	     (:copier nil))
  (term nil :read-only t))

(defun make-tree-index (&key (entry-constructor #'make-index-entry))
  (setf *tree-index* (make-tree-index0 entry-constructor)))

(definline tree-index-internal-node-variable-indexed-child-node (node &optional create internal)
  (or (tree-index-internal-node-variable-child-node node)
      (and create
           (progn
             (increment-counter (tree-index-node-counter *tree-index*))
             (setf (tree-index-internal-node-variable-child-node node)
                   (if internal
                       (make-tree-index-internal-node :parent-node node)
                       (make-tree-index-leaf-node :parent-node node)))))))

(definline tree-index-internal-node-constant-indexed-child-node (const node &optional create internal)
  (let ((children (tree-index-internal-node-constant-indexed-child-nodes node)))
    (unless children
      (when create
        (setf children (setf (tree-index-internal-node-constant-indexed-child-nodes node) (make-sparse-vector)))))
    (and children
         (let ((const# (constant-number const)))
           (or (sparef children const#)
               (and create
                    (progn
                      (increment-counter (tree-index-node-counter *tree-index*))
                      (setf (sparef children const#)
                            (if internal
                                (make-tree-index-internal-node :parent-node node)
                                (make-tree-index-leaf-node :parent-node node))))))))))

(definline tree-index-internal-node-function-indexed-child-node (fn node &optional create internal)
  (let ((children (tree-index-internal-node-function-indexed-child-nodes node)))
    (unless children
      (when create
        (setf children (setf (tree-index-internal-node-function-indexed-child-nodes node) (make-sparse-vector)))))
    (and children
         (let ((fn# (function-number fn)))
           (or (sparef children fn#)
               (and create
                    (progn
                      (increment-counter (tree-index-node-counter *tree-index*))
                      (setf (sparef children fn#)
                            (if internal
                                (make-tree-index-internal-node :parent-node node)
                                (make-tree-index-leaf-node :parent-node node))))))))))

(definline tree-indexable-args (fn &optional term lookup)
  ;; returns 0 or nil for terms headed by functions that cannot be tree indexed, etc.
  ;; fn = (head term) unless term is nil (not specified)
  ;; if term is not specified, return number of tree-indexable arguments
  ;; if term is specifed, return tree-indexable-arguments or,
  ;; if lookup is true, possibly includes expressions like (%index-or args1 ... argsn) for index-tree lookup
  (ecase (function-index-type fn)
    ((nil)
     (cond
      ((function-unify-code fn)
       (if term nil 0))
      (t
       (let ((arity (function-arity fn)))
         (cond
          ((eq :any arity)
           (if term nil 0))
          ((eq :list* arity)
           (if term (args term) 1))
          (t
           (if term (args term) arity)))))))
    (:commute2
     ;; index only first two arguments, lookup with first two in order and commuted
     ;; (a b c) -> 2, (a b), ((%index-or (a b) (b a)))
     (if term
         (let ((args (let ((args (args term)))
                       (if (rest (rest args)) (list (first args) (second args)) args))))
           (if lookup (list (list '%index-or args (list (second args) (first args)))) args))
         2))
    (:commute
     ;; index all arguments, lookup with first two in order and commuted
     ;; (a b c) -> 3, (c a b), (c (%index-or (a b) (b a)))
     (if term
         (let* ((args (args term))
                (a (first args))
                (b (second args))
                (l (rest (rest args))))
           (if l
               (append l (if lookup (list (list '%index-or (list a b) (list b a))) (list a b)))
               (if lookup (list (list '%index-or args (list* (second args) (first args)))) args)))
         (function-arity fn)))))

(defun tree-index-build-path-for-term (term node &optional internal)
  (dereference
   term nil
   :if-variable (tree-index-internal-node-variable-indexed-child-node node t internal)
   :if-constant (tree-index-internal-node-constant-indexed-child-node term node t internal)
   :if-compound (let* ((head (head term))
                       (args (tree-indexable-args head term)))
                  (if (null args)
                      (tree-index-internal-node-function-indexed-child-node head node t internal)
                      (tree-index-build-path-for-terms args (tree-index-internal-node-function-indexed-child-node head node t t) internal)))))

(defun tree-index-build-path-for-terms (terms node internal)
  (if internal
      (dolist (x terms node)
        (setf node (tree-index-build-path-for-term x node t)))
      (dotails (l terms node)
        (setf node (tree-index-build-path-for-term (first l) node (rest l))))))

(defun tree-index-insert (term)
  (let* ((tree-index *tree-index*)
         (leaf-node (tree-index-build-path-for-term term (tree-index-top-node tree-index)))
         (entries (tree-index-leaf-node-entries leaf-node)))
    (prog->
      (map-sparse-vector entries ->* entry)
      (when (eql term (index-entry-term entry))
        (return-from tree-index-insert entry)))
    (let ((entry (funcall (tree-index-entry-constructor tree-index) term)))
      (increment-counter (tree-index-entry-counter tree-index))
      (setf (sparef entries (- (nonce))) entry)
      entry)))

(defun tree-index-insert-entry (entry)
  (let* ((term (index-entry-term entry))
         (tree-index *tree-index*)
         (leaf-node (tree-index-build-path-for-term term (tree-index-top-node tree-index)))
         (entries (tree-index-leaf-node-entries leaf-node)))
    (let ((found-term nil))
      (prog->
        (map-sparse-vector entries ->* e)
        (when (eql term (index-entry-term e))
          (cond
           ((eq entry e)
            (return-from tree-index-insert-entry entry))
           ((not found-term)
            (warn "There is already a tree-index entry for term ~A." term)
            (setf found-term t))))))
    (increment-counter (tree-index-entry-counter tree-index))
    (setf (sparef entries (- (nonce))) entry)
    entry))

(defun tree-index-delete (term)
  (let* ((tree-index *tree-index*)
         (leaf-node (tree-index-build-path-for-term term (tree-index-top-node tree-index)))
         (entries (tree-index-leaf-node-entries leaf-node))
         (deleted nil))
    (prog->
      (map-sparse-vector-with-indexes entries ->* entry index)
      (when (eql term (index-entry-term entry))
        (decrement-counter (tree-index-entry-counter tree-index))
        (setf (sparef entries index) none)
        (setf deleted t)))
    (when deleted
      (when (and (eql 0 (sparse-vector-count entries)) (delete-empty-index-nodes?))
        (tree-index-delete-node-from-parent leaf-node (tree-index-node-counter tree-index)))
      t)))

(defun tree-index-delete-entry (entry)
  (let* ((term (index-entry-term entry))
         (tree-index *tree-index*)
         (leaf-node (tree-index-build-path-for-term term (tree-index-top-node tree-index)))
         (entries (tree-index-leaf-node-entries leaf-node))
         (deleted nil))
    (prog->
      (map-sparse-vector-with-indexes entries ->* e index)
      (when (eq entry e)
        (decrement-counter (tree-index-entry-counter tree-index))
        (setf (sparef entries index) none)
        (setf deleted t)))
    (when deleted
      (when (and (eql 0 (sparse-vector-count entries)) (delete-empty-index-nodes?))
        (tree-index-delete-node-from-parent leaf-node (tree-index-node-counter tree-index)))
      t)))

(defun tree-index-key-for-value (value table)
  (map-sparse-vector-with-indexes
   (lambda (v k)
     (when (eq value v)
       (return-from tree-index-key-for-value k)))
   table))

(defun tree-index-delete-node-from-parent (node &optional counter)
  (when counter
    (decrement-counter counter))
  (let ((parent (tree-index-node-parent-node node)))
    (when parent
      (let ((constant-indexed-children (tree-index-internal-node-constant-indexed-child-nodes parent))
            (function-indexed-children (tree-index-internal-node-function-indexed-child-nodes parent))
            v)
        (cond
         ((eq node (tree-index-internal-node-variable-child-node parent))
          (setf (tree-index-internal-node-variable-child-node parent) nil))
         ((setf v (tree-index-key-for-value node constant-indexed-children))
          (setf (sparef constant-indexed-children v) nil))
         ((setf v (tree-index-key-for-value node function-indexed-children))
          (setf (sparef function-indexed-children v) nil))
         (t
          (error "couldn't find leaf node in parent.")))
        (when (and (null (tree-index-internal-node-variable-child-node parent))
                   (eql 0 (sparse-vector-count constant-indexed-children))
                   (eql 0 (sparse-vector-count function-indexed-children)))
          (tree-index-delete-node-from-parent parent counter))))))

(defmacro map-tree-index-entries (&key if-variable if-constant if-compound)
  `(labels
     ((map-for-term (cc term node)
        (dereference
         term subst
         :if-variable ,if-variable
         :if-constant ,if-constant
         :if-compound ,if-compound))
      (map-for-terms (cc terms node)
        (cond
         ((null terms)
          (funcall cc node))
         (t
          (let ((term (pop terms)))
            (cond
             ((and (consp term) (eq '%index-or (first term)))
              (cond
               ((null terms)
                (prog->
                  (dolist (rest term) ->* terms1)
                  (map-for-terms terms1 node ->* node)
                  (funcall cc node)))
               (t
                (prog->
                  (dolist (rest term) ->* terms1)
                  (map-for-terms terms1 node ->* node)
                  (map-for-terms terms node ->* node)
                  (funcall cc node)))))
             (t
              (cond
               ((null terms)
                (prog->
                  (map-for-term term node ->* node)
                  (funcall cc node)))
               (t
                (prog->
                  (map-for-term term node ->* node)
                  (map-for-terms terms node ->* node)
                  (funcall cc node))))))))))
      (skip-terms (cc n node)
        (declare (type fixnum n))
        (cond
         ((= 1 n)
          (progn
            (prog->
              (tree-index-internal-node-variable-indexed-child-node node ->nonnil node)
              (funcall cc node))
            (prog->
              (tree-index-internal-node-constant-indexed-child-nodes node ->nonnil constant-indexed-children)
              (map-sparse-vector constant-indexed-children ->* node)
              (funcall cc node))
            (prog->
              (tree-index-internal-node-function-indexed-child-nodes node ->nonnil function-indexed-children)
              (map-sparse-vector-with-indexes function-indexed-children ->* node fn#)
              (skip-terms (tree-indexable-args (symbol-numbered fn#)) node ->* node)
              (funcall cc node))))
         ((= 0 n)
          (funcall cc node))
         (t
          (progn
            (decf n)
            (prog->
              (tree-index-internal-node-variable-indexed-child-node node ->nonnil node)
              (skip-terms n node ->* node)
              (funcall cc node))
            (prog->
              (tree-index-internal-node-constant-indexed-child-nodes node ->nonnil constant-indexed-children)
              (map-sparse-vector constant-indexed-children ->* node)
              (skip-terms n node ->* node)
              (funcall cc node))
            (prog->
              (tree-index-internal-node-function-indexed-child-nodes node ->nonnil function-indexed-children)
              (map-sparse-vector-with-indexes function-indexed-children ->* node fn#)
              (skip-terms (+ n (tree-indexable-args (symbol-numbered fn#))) node ->* node)
              (funcall cc node)))))))
     (prog->
       (cons 'query-id nil -> query-id)
       (map-for-term term (tree-index-top-node *tree-index*) ->* leaf-node)
       (unless (eq query-id (tree-index-leaf-node-mark leaf-node))
         (setf (tree-index-leaf-node-mark leaf-node) query-id)
         (map-sparse-vector (tree-index-leaf-node-entries leaf-node) ->* e)
         (funcall cc e)))
     nil))

(defun map-tree-index-instance-entries (cc term &optional subst)
  (map-tree-index-entries
   :if-variable (prog->
                  (skip-terms 1 node ->* node)
                  (funcall cc node))
   :if-constant (prog->
                  (tree-index-internal-node-constant-indexed-child-node term node ->nonnil node)
                  (funcall cc node))
   :if-compound (prog->
                  (head term -> head)
                  (tree-index-internal-node-function-indexed-child-node head node ->nonnil node)
                  (map-for-terms (tree-indexable-args head term t) node ->* node)
                  (funcall cc node))))

(defun map-tree-index-generalization-entries (cc term &optional subst)
  ;; in snark-20060805 vs. snark-20060806 test over TPTP,
  ;; constant and compound lookup before variable lookup outperforms
  ;; variable lookup before constant and compount lookup
  (map-tree-index-entries
   :if-variable (prog->
                  (tree-index-internal-node-variable-indexed-child-node node ->nonnil node)
                  (funcall cc node))
   :if-constant (progn
                  (prog->
                    (tree-index-internal-node-constant-indexed-child-node term node ->nonnil node)
                    (funcall cc node))
                  (prog->
                    (tree-index-internal-node-variable-indexed-child-node node ->nonnil node)
                    (funcall cc node)))
   :if-compound (progn
                  (prog->
                    (head term -> head)
                    (tree-index-internal-node-function-indexed-child-node head node ->nonnil node)
                    (map-for-terms (tree-indexable-args head term t) node ->* node)
                    (funcall cc node))
                  (prog->
                    (tree-index-internal-node-variable-indexed-child-node node ->nonnil node)
                    (funcall cc node)))))

(defun map-tree-index-unifiable-entries (cc term &optional subst)
  (map-tree-index-entries
   :if-variable (prog->
                  (skip-terms 1 node ->* node)
                  (funcall cc node))
   :if-constant (progn
                  (prog->
                    (tree-index-internal-node-variable-indexed-child-node node ->nonnil node)
                    (funcall cc node))
                  (prog->
                    (tree-index-internal-node-constant-indexed-child-node term node ->nonnil node)
                    (funcall cc node)))
   :if-compound (progn
                  (prog->
                    (tree-index-internal-node-variable-indexed-child-node node ->nonnil node)
                    (funcall cc node))
                  (prog->
                    (head term -> head)
                    (tree-index-internal-node-function-indexed-child-node head node ->nonnil node)
                    (map-for-terms (tree-indexable-args head term t) node ->* node)
                    (funcall cc node)))))

(defun map-tree-index-variant-entries (cc term &optional subst)
  (map-tree-index-entries
   :if-variable (prog->
                  (tree-index-internal-node-variable-indexed-child-node node ->nonnil node)
                  (funcall cc node))
   :if-constant (prog->
                  (tree-index-internal-node-constant-indexed-child-node term node ->nonnil node)
                  (funcall cc node))
   :if-compound (prog->
                  (head term -> head)
                  (tree-index-internal-node-function-indexed-child-node head node ->nonnil node)
                  (map-for-terms (tree-indexable-args head term t) node ->* node)
                  (funcall cc node))))

(defun print-tree-index (&key terms nodes)
  (let ((index *tree-index*))
    (mvlet (((:values current peak added deleted) (counter-values (tree-index-entry-counter index))))
      (format t "~%; Tree-index has ~D entr~:@P (~D at peak, ~D added, ~D deleted)." current peak added deleted))
    (mvlet (((:values current peak added deleted) (counter-values (tree-index-node-counter index))))
      (format t "~%; Tree-index has ~D node~:P (~D at peak, ~D added, ~D deleted)." current peak added deleted))
    (when (or nodes terms)
      (print-index* (tree-index-top-node index) nil terms))))

(defun print-index* (node revpath print-terms)
  (prog->
    (map-index-leaf-nodes node revpath ->* node revpath)
    (print-index-leaf-node node revpath print-terms)))

(defmethod map-index-leaf-nodes (cc (node tree-index-internal-node) revpath)
  (prog->
    (tree-index-internal-node-variable-indexed-child-node node ->nonnil node)
    (map-index-leaf-nodes node (cons '? revpath) ->* node revpath)
    (funcall cc node revpath))
  (prog->
    (map-sparse-vector-with-indexes (tree-index-internal-node-constant-indexed-child-nodes node) ->* node const#)
    (map-index-leaf-nodes node (cons (symbol-numbered const#) revpath) ->* node revpath)
    (funcall cc node revpath))
  (prog->
    (map-sparse-vector-with-indexes (tree-index-internal-node-function-indexed-child-nodes node) ->* node fn#)
    (map-index-leaf-nodes node (cons (symbol-numbered fn#) revpath) ->* node revpath)
    (funcall cc node revpath)))

(defmethod map-index-leaf-nodes (cc (node tree-index-leaf-node) revpath)
  (funcall cc node revpath))

(defmethod print-index-leaf-node ((node tree-index-leaf-node) revpath print-terms)
  (with-standard-io-syntax2
    (prog->
      (tree-index-leaf-node-entries node -> entries)
      (format t "~%; Path ~A has ~D entr~:@P." (reverse revpath) (length entries))
      (when print-terms
        (dolist entries ->* entry)
        (format t "~%;    ")
        (print-term (index-entry-term entry))))))

;;; tree-index.lisp EOF
